0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 277 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 24 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
palindromeB_in_g([]) → palindromeB_out_g([])
palindromeB_in_g(.(T19, [])) → palindromeB_out_g(.(T19, []))
palindromeB_in_g(.(T42, .(T42, []))) → palindromeB_out_g(.(T42, .(T42, [])))
palindromeB_in_g(.(T75, .(T74, .(T75, [])))) → palindromeB_out_g(.(T75, .(T74, .(T75, []))))
palindromeB_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeB_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeB_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeB_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeB_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeB_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeB_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeB_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeB_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseA_in_ggggg([], T365, T366, T365, T366) → reverseA_out_ggggg([], T365, T366, T365, T366)
reverseA_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseA_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeB_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
palindromeB_in_g([]) → palindromeB_out_g([])
palindromeB_in_g(.(T19, [])) → palindromeB_out_g(.(T19, []))
palindromeB_in_g(.(T42, .(T42, []))) → palindromeB_out_g(.(T42, .(T42, [])))
palindromeB_in_g(.(T75, .(T74, .(T75, [])))) → palindromeB_out_g(.(T75, .(T74, .(T75, []))))
palindromeB_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeB_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeB_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeB_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeB_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeB_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeB_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeB_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeB_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseA_in_ggggg([], T365, T366, T365, T366) → reverseA_out_ggggg([], T365, T366, T365, T366)
reverseA_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseA_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeB_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROMEB_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_G(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROMEB_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → REVERSEA_IN_GGGGG(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))
REVERSEA_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → U1_GGGGG(T379, T380, T381, T382, T383, T384, reverseA_in_ggggg(T380, T379, .(T381, T382), T383, T384))
REVERSEA_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEA_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)
palindromeB_in_g([]) → palindromeB_out_g([])
palindromeB_in_g(.(T19, [])) → palindromeB_out_g(.(T19, []))
palindromeB_in_g(.(T42, .(T42, []))) → palindromeB_out_g(.(T42, .(T42, [])))
palindromeB_in_g(.(T75, .(T74, .(T75, [])))) → palindromeB_out_g(.(T75, .(T74, .(T75, []))))
palindromeB_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeB_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeB_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeB_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeB_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeB_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeB_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeB_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeB_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseA_in_ggggg([], T365, T366, T365, T366) → reverseA_out_ggggg([], T365, T366, T365, T366)
reverseA_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseA_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeB_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROMEB_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_G(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROMEB_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → REVERSEA_IN_GGGGG(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))
REVERSEA_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → U1_GGGGG(T379, T380, T381, T382, T383, T384, reverseA_in_ggggg(T380, T379, .(T381, T382), T383, T384))
REVERSEA_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEA_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)
palindromeB_in_g([]) → palindromeB_out_g([])
palindromeB_in_g(.(T19, [])) → palindromeB_out_g(.(T19, []))
palindromeB_in_g(.(T42, .(T42, []))) → palindromeB_out_g(.(T42, .(T42, [])))
palindromeB_in_g(.(T75, .(T74, .(T75, [])))) → palindromeB_out_g(.(T75, .(T74, .(T75, []))))
palindromeB_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeB_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeB_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeB_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeB_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeB_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeB_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeB_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeB_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseA_in_ggggg([], T365, T366, T365, T366) → reverseA_out_ggggg([], T365, T366, T365, T366)
reverseA_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseA_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeB_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
REVERSEA_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEA_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)
palindromeB_in_g([]) → palindromeB_out_g([])
palindromeB_in_g(.(T19, [])) → palindromeB_out_g(.(T19, []))
palindromeB_in_g(.(T42, .(T42, []))) → palindromeB_out_g(.(T42, .(T42, [])))
palindromeB_in_g(.(T75, .(T74, .(T75, [])))) → palindromeB_out_g(.(T75, .(T74, .(T75, []))))
palindromeB_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeB_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeB_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeB_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeB_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeB_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeB_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeB_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeB_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseA_in_ggggg([], T365, T366, T365, T366) → reverseA_out_ggggg([], T365, T366, T365, T366)
reverseA_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverseA_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseA_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseA_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeB_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
REVERSEA_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEA_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)
REVERSEA_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEA_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)
From the DPs we obtained the following set of size-change graphs: